parser grammar TBTParser;

options{
	tokenVocab = TBTLexer;
	language = Java;
	output = AST;
}

tokens{
  PROG;
  PROLOG;
  TERM;
  TL_BINDING;
  TL_BINDINGS;

// Terms syntax
  LAM_ABS;
  LAM_APP;
  VAR;
  
  TYPE_ABS;
  TYPE_APP;
  TVAR;
  
  BRANCHES;
  BRANCH;

// Types syntax  
  FUNCTION;
  FOR_ALL;
  TCONS_APP;
    
  DATATYPE;
  TARGS;
  TCONSTRUCTORS;
  TCONS;

// Stared type
  STARED_TYPE;
}
@header {
	package parser;
	import java.util.Set;
	import java.util.HashSet;
}

@members {
  // Arrow is right associative
  private Tree createArrowTree(Tree first , List rest, List arrows){
    Tree crt , root1;
      
    rest.add(0,first);
    crt = (Tree)rest.get(rest.size()-1);
    
    for( int i = rest.size()-2; i >= 0; i--){
      Tree tmpRoot = (Tree)adaptor.nil();
      adaptor.addChild( tmpRoot, rest.get(i));
      adaptor.addChild( tmpRoot, crt);
      crt = (Tree) adaptor.becomeRoot( (Token) arrows.get(i), tmpRoot);
    }

    return crt;
  }
  private Set<String> ctors = new HashSet<String>();
  
}

program 
    : prolog tl_binding* term -> ^(PROG prolog ^(TL_BINDINGS tl_binding*) ^(TERM term) );

prolog 
    : datatype* -> ^(PROLOG datatype*);

/* We could infer the type of the top-level bounded variables, but we prefer not to */
tl_binding
    : LET LANG type RANG ID BIND term COLUMN -> ^(TL_BINDING ID type term)
    ;
    
/* Type grammar */
arrow : ARROW;
star_type : type ;
type 
@init{
  List rest = new ArrayList();
  List arrows = new ArrayList();
}
    : FORALL TID DOT type
        -> ^(FOR_ALL TID type)
    | first=type_app ((ARROW)=>arrow ta=type_app {arrows.add($arrow.start); rest.add($ta.tree);} )* 
      -> {createArrowTree((Tree)$first.tree, rest, arrows)}    
    ;

type_app
    : tid_star (type_atom)+ 
        -> ^(TCONS_APP tid_star type_atom*) 
    | type_atom
    ;
  
type_atom
    : c=tid_star
        -> {ctors.contains($c.name)}? ^(TCONS_APP $c)
        -> tid_star
    | LPAREN type RPAREN  -> type
    ;

tid_star returns [String name]
    /* we make no difference between starred types an raw ones at sintactic level */
    : TID STAR  {$name = $TID.text; } -> ^(TVAR ^(STARED_TYPE TID)) 
    | TID       {$name = $TID.text; } -> ^(TVAR TID)
    ;
    
/* Lambda term grammar  */
term 
    : (term_atom -> term_atom) 
                ( (LANG)=> LANG type RANG -> ^(TYPE_APP $term type)
                | (term_atom) => term_atom -> ^(LAM_APP $term term_atom)
                )* 
    ;
    
term_atom
    : LPAREN term RPAREN
      -> term
    | TLAMBDA TID DOT term
      -> ^(TYPE_ABS TID term)
    | LAMBDA LANG type RANG ID  DARROW term
      -> ^(LAM_ABS ID type term)
    | LETREC LANG star_type RANG ID BIND term 
      -> ^(LETREC star_type ID term)
    | CASE LANG type RANG term OF LCURLY variant (OR variant)* RCURLY
      -> ^(CASE type term ^(BRANCHES variant*))
    | ID
      -> ^(VAR ID)
    ;

variant 
    : ID DARROW term
      -> ^(BRANCH ID term)
    ;

/* Sized datatype grammar */
datatype 
    : IND name=TID {ctors.add($name.text);} tid* EQ constr (OR constr)* COLUMN 
      -> ^(DATATYPE $name ^(TARGS tid*) ^(TCONSTRUCTORS constr*) )
    ; 
tid : TID;
   
constr
    : ID SEMI type
      -> ^(TCONS ID type)
    ;
    
